InforLorV4, Main, Exploration, bibRecord, 002618

Towards Verification of the Pastry Protocol Using TLA +

Identifieur interne : 002618 ( Main/Exploration ); précédent : 002617; suivant : 002619

Towards Verification of the Pastry Protocol Using TLA +

Auteurs : Tianxiang Lu [Allemagne, France] ; Stephan Merz [France] ; Christoph Weidenbach [Allemagne]

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:0D726DA2F51FE28ABFD0FD669CC9D07C991EF136

Abstract

Abstract: Pastry is an algorithm that provides a scalable distributed hash table over an underlying P2P network. Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to churn and fault tolerance, it makes an interesting target for verification. We have modeled Pastry’s core routing algorithms and communication protocol in the specification language TLA + . In order to validate the model and to search for bugs we employed the TLA + model checker tlc to analyze several qualitative properties. We obtained non-trivial insights in the behavior of Pastry through the model checking analysis. Furthermore, we started to verify Pastry using the very same model and the interactive theorem prover tlaps for TLA + . A first result is the reduction of global Pastry correctness properties to invariants of the underlying data structures.

Url:

https://api.istex.fr/ark:/67375/HCB-BQDVF9LH-X/fulltext.pdf

DOI: 10.1007/978-3-642-21461-5_16

Affiliations:

Links toward previous steps (curation, corpus...)

to stream Istex, to step Corpus: 000293
to stream Istex, to step Curation: 000292
to stream Istex, to step Checkpoint: 000518
to stream Main, to step Merge: 002660
to stream Main, to step Curation: 002618

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Towards Verification of the Pastry Protocol Using TLA + </title>
<author><name sortKey="Lu, Tianxiang" sort="Lu, Tianxiang" uniqKey="Lu T" first="Tianxiang" last="Lu">Tianxiang Lu</name>
</author>
<author><name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name>
</author>
<author><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:0D726DA2F51FE28ABFD0FD669CC9D07C991EF136</idno>
<date when="2011" year="2011">2011</date>
<idno type="doi">10.1007/978-3-642-21461-5_16</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-BQDVF9LH-X/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">000293</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000293</idno>
<idno type="wicri:Area/Istex/Curation">000292</idno>
<idno type="wicri:Area/Istex/Checkpoint">000518</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000518</idno>
<idno type="wicri:doubleKey">0302-9743:2011:Lu T:towards:verification:of</idno>
<idno type="wicri:Area/Main/Merge">002660</idno>
<idno type="wicri:Area/Main/Curation">002618</idno>
<idno type="wicri:Area/Main/Exploration">002618</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Towards Verification of the Pastry Protocol Using TLA<hi rend="superscript"> + </hi>
</title>
<author><name sortKey="Lu, Tianxiang" sort="Lu, Tianxiang" uniqKey="Lu T" first="Tianxiang" last="Lu">Tianxiang Lu</name>
<affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country>
<wicri:regionArea>Max-Planck-Institut für Informatik, Saarbrücken</wicri:regionArea>
<placeName><region type="land" nuts="2">Sarre (Land)</region>
<settlement type="city">Sarrebruck</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>INRIA Nancy & LORIA, Nancy</wicri:regionArea>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>INRIA Nancy & LORIA, Nancy</wicri:regionArea>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name>
<affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country>
<wicri:regionArea>Max-Planck-Institut für Informatik, Saarbrücken</wicri:regionArea>
<placeName><region type="land" nuts="2">Sarre (Land)</region>
<settlement type="city">Sarrebruck</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: Pastry is an algorithm that provides a scalable distributed hash table over an underlying P2P network. Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to churn and fault tolerance, it makes an interesting target for verification. We have modeled Pastry’s core routing algorithms and communication protocol in the specification language TLA + . In order to validate the model and to search for bugs we employed the TLA +  model checker tlc to analyze several qualitative properties. We obtained non-trivial insights in the behavior of Pastry through the model checking analysis. Furthermore, we started to verify Pastry using the very same model and the interactive theorem prover tlaps for TLA + . A first result is the reduction of global Pastry correctness properties to invariants of the underlying data structures.</div>
</front>
</TEI>
<affiliations><list><country><li>Allemagne</li>
<li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
<li>Sarre (Land)</li>
</region>
<settlement><li>Nancy</li>
<li>Sarrebruck</li>
</settlement>
</list>
<tree><country name="Allemagne"><region name="Sarre (Land)"><name sortKey="Lu, Tianxiang" sort="Lu, Tianxiang" uniqKey="Lu T" first="Tianxiang" last="Lu">Tianxiang Lu</name>
</region>
<name sortKey="Lu, Tianxiang" sort="Lu, Tianxiang" uniqKey="Lu T" first="Tianxiang" last="Lu">Tianxiang Lu</name>
<name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name>
<name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name>
</country>
<country name="France"><region name="Grand Est"><name sortKey="Lu, Tianxiang" sort="Lu, Tianxiang" uniqKey="Lu T" first="Tianxiang" last="Lu">Tianxiang Lu</name>
</region>
<name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name>
<name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002618 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 002618 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     ISTEX:0D726DA2F51FE28ABFD0FD669CC9D07C991EF136
   |texte=   Towards Verification of the Pastry Protocol Using TLA + 
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Towards Verification of the Pastry Protocol Using TLA +

Towards Verification of the Pastry Protocol Using TLA +

Source :

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri